Example 9 in [Lucas - FOSSACS'04]

Summary: Ex9_Luc04

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas', Zantema's, Ferreira and Ribeiro's transformations, and Giesl and Middeldorp's transformation
  2. CSRPO
• Positive results:
  1. Polynomial fractions
  2. CSDP

CS-TRS Ex9_Luc04 (file Ex9_Luc04.csr)

Functions:  f a b c

Constructors:  a b

Variables:  X

Arities: 

ar(f) = 3
ar(a) = 0
ar(b) = 0
ar(c) = 0

Replacement map: 

µ(f)={1,3}
µ(a)={}
µ(b)={}
µ(c)={}

Rules:  (file Ex9_Luc04)

f(a,b,X) -> f(X,X,X)
c -> a
c -> b

The CS-TRS in OBJ format (file Ex9_Luc04.obj):

obj Ex9_Luc04 is
  sort S .
  op f : S S S -> S [strat (1 3 0)] .
  op a : -> S .
  op b : -> S .
  op c : -> S .
  vars X : S .
  eq f(a,b,X) = f(X,X,X) .
  eq c = a .
  eq c = b .
endo

Negative results

1. The µ-termination of Ex9_Luc04 cannot be proved terminating by either Lucas', Zantema's, Ferreira and Ribeiro's, or Giesl and Middeldorp's transformations [GM99, Example 1; GM04, Example 15].
2. The mu-termination of Ex9_Luc04 cannot be proved by using CSRPO [GL02b, Section 5.1].

Positive results

1. The µ-termination of Ex9_Luc04 is proved in [Luc04, Example 9] by using the following interpretation:

      [f](x,y,z) = [(xy + z)+(x + yz)]/y 
         = [x(y+1) + z(y+1)]/y 
         = x + zy^-1 + xy^-1 + z
      [a] = 2
      [b] = 1
      [c] = 3
      

2. The µ-termination of Ex9_Luc04 can also be proved by using CSDP:

   There is only one dependency pair:

   	F(a,b,X) -> F(X,X,X)
   

   with µ(F)={1,3}. Although there is a cycle in the dependency graph, no infinite chain is possible due to the replacement restrictions for F.